﻿#ifndef ModelCreate
#define ModelCreate
#include"Header.h"
#include <algorithm>
#include <random>

struct State //存储单个状态内容
{
    int ID;									//状态编号
    set<char> atom_set;					//标记的原子公式子集
    set<int> B_set;							//与当前状态有belief关系的状态子集
    set<set<int> > P_sets;					//与当前状态有preference关系的若干状态子集
    set<set<int> > I_sets;					//与当前状态有intention关系的若干状态子集
    set<int> X_set;							//与当前状态有时序关系的状态子集
    set<int> formula_set;				//标记当前状态下成立的公式
    set<int> F_set;					//标记当前状态的父结点状态
    int dfn = 0;//DFS中被访问的时间点
    int low = 0;//通过有向边可回溯到的最早的时间点
    bool operator <(const State& obj) const {
        return ID < obj.ID;
    }
};

set<char> atom_set; //输入模型原子公式集
vector<State*> state_set; //输入模型状态集
map<string, int> state_id_map; //状态-id转换映射
map<int, State*> id_state_map; //id-状态转换映射
set<int> state_id_set; //输入模型状态id集合
set<set<int> > D_set; //D集合
set<pair<int, int> > RX; //RX集合
set<pair<int, int> > rt_closure; //RX的自反传递闭包
vector<set<int>> SCC_set;

void calc_D_set(set<int> S)
{
    if (S.size() == 1)
        return;
    set<int> T;

    D_set.insert(state_id_set);
    for (int s : S)
    {
        T = S;
        T.erase(s);
        D_set.insert(T);
        calc_D_set(T);
    }
}
int turn_id(string s)
{
    int num = 0;

    for (int i = 1; i < s.length(); i++)
    {
        num *= 10;
        num += s[i] - '0';
    }
    return num;
}
void init_state(string f1, string f2)
{
    fstream file1, file2;
    char temp_atom;
    string temp_state;
    set<int> temp_state_set;
    State* state = NULL, * child;
    int id;

    file1.open(f1, ios::in);
    if (file1.fail())
    {
        cout << "文件打开失败！" << endl;
        exit(0);
    }
    while (!file1.eof()) //输入原子公式
    {
        file1 >> temp_atom;
        if (temp_atom == '#')
            break;
        atom_set.insert(temp_atom);
    }
    int no = 0;
    while (!file1.eof()) //输入状态并转换为编号
    {
        file1 >> temp_state;
        if (temp_state[0] == '#')
            break;
        no = turn_id(temp_state);
        state_id_set.insert(no);
        state_id_map.insert(make_pair(temp_state, no));
        state = new State;
        state->ID = no;
        state_set.push_back(state);
        id_state_map[state->ID] = state;
    }
    file1.close();

    file2.open(f2, ios::in);
    if (file2.fail())
    {
        cout << "文件打开失败！" << endl;
        exit(0);
    }
    while (1)
    {
        file2 >> temp_state;
        if (file2.eof())
            break;
        id = state_id_map[temp_state];
        state = id_state_map[id];

        file2 >> temp_atom;
        while (temp_atom != '#') //原子公式
        {
            state->atom_set.insert(temp_atom);
            file2 >> temp_atom;
        }

        file2 >> temp_state;
        while (temp_state[0] != '#') //B
        {
            state->B_set.insert(state_id_map[temp_state]);
            file2 >> temp_state;
            if (temp_state == "-")
                file2 >> temp_state;
        }

        file2 >> temp_state;
        if (temp_state != "#")
        {
            while (1) //P
            {
                if (temp_state[0] == '-' || temp_state[0] == '#')
                {
                    state->P_sets.insert(temp_state_set);
                    temp_state_set.clear();
                    if (temp_state[0] == '#')
                        break;
                }
                else
                    temp_state_set.insert(state_id_map[temp_state]);
                file2 >> temp_state;
            }
        }

        file2 >> temp_state;
        if (temp_state != "#")
        {
            while (1) //I
            {
                if (temp_state[0] == '-' || temp_state[0] == '#')
                {
                    state->I_sets.insert(temp_state_set);
                    temp_state_set.clear();
                    if (temp_state[0] == '#')
                        break;
                }
                else
                    temp_state_set.insert(state_id_map[temp_state]);
                file2 >> temp_state;
            }
        }

        file2 >> temp_state;
        while (temp_state[0] != '#') //X
        {
            id = state_id_map[temp_state];
            state->X_set.insert(id);
            child = id_state_map[id];
            child->F_set.insert(state->ID);

            RX.insert(make_pair(state->ID, id)); //RX

            file2 >> temp_state;
        }
    }
    file2.close();
}
void ModelPrint()
{
    State* s;
    //输出模型状态集
    for (int i = 0; i < state_set.size(); i++)
    {
        s = state_set[i];
        cout << "状态名：" << s->ID << endl;
        cout << "原子公式集：";
        for (set<char>::iterator p = s->atom_set.begin(); p != s->atom_set.end(); p++)
            cout << *p << ' ';
        cout << endl;

        cout << "B集：";
        for (set<int>::iterator p = s->B_set.begin(); p != s->B_set.end(); p++)
            cout << *p << ' ';
        cout << endl;

        cout << "P集：";
        for (set<set<int> >::iterator p = s->P_sets.begin(); p != s->P_sets.end(); p++)
        {
            for (set<int>::iterator q = p->begin(); q != p->end(); q++)
                cout << *q << ' ';
            cout << "# ";
        }
        cout << endl;

        cout << "I集：";
        for (set<set<int> >::iterator p = s->I_sets.begin(); p != s->I_sets.end(); p++)
        {
            for (set<int>::iterator q = p->begin(); q != p->end(); q++)
                cout << *q << ' ';
            cout << "# ";
        }
        cout << endl;

        cout << "X集：";
        for (set<int>::iterator p = s->X_set.begin(); p != s->X_set.end(); p++)
            cout << *p << ' ';
        cout << endl;

        cout << "满足的公式集:" << endl;
        for (set<int>::iterator p = s->formula_set.begin(); p != s->formula_set.end(); p++)
            cout << *p << ' ';
        cout << endl;
        cout << "F集：" << endl;
        for (int p : s->F_set)
            cout << p << ' ';
        cout << endl << endl;
    }
}
bool condition_B3()
{
    State* x;

    for (int i = 0; i < state_set.size(); i++) //遍历x
    {
        x = state_set[i];
        for (int y_id : x->B_set) //遍历y
        {
            for (int z_id : id_state_map[y_id]->B_set) //遍历z
            {
                if (x->B_set.find(z_id) == x->B_set.end())
                    return false;
            }
        }
    }
    return true;
}
bool condition_B4()
{
    State* x, * y;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (int y_id : x->B_set)
        {
            for (int z_id : x->B_set)
            {
                y = id_state_map[y_id];
                if (y->B_set.find(z_id) == y->B_set.end())
                    return false;
            }
        }
    }
    return true;
}
bool condition_B5()
{
    for (int i = 0; i < state_set.size(); i++)
    {
        if (state_set[i]->B_set.size() == 0)
            return false;
    }
    return true;
}
bool condition_P1()
{
    set<int> U;

    for (int i = 0; i < state_set.size(); i++)
    {
        for (set<int> Q1 : state_set[i]->P_sets)
        {
            for (set<int> Q2 : state_set[i]->P_sets)
            {
                set_intersection(Q1.begin(), Q1.end(), Q2.begin(), Q2.end(),
                    std::inserter(U, U.begin())); //Q1 交 Q2
                if (state_set[i]->P_sets.find(U) == state_set[i]->P_sets.end())
                    return false;
            }
        }
    }
    return true;
}
bool condition_P2()
{
    State* x;
    set<int> U, T, Q2;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q1 : x->P_sets)
        {
            set_difference(state_id_set.begin(), state_id_set.end(),
                Q1.begin(), Q1.end(), std::inserter(U, U.begin())); //Q1补
            for (set<int> Q2 : D_set)
            {
                set_union(U.begin(), U.end(), Q2.begin(), Q2.end(),
                    std::inserter(T, T.begin())); //Q1补 ∪ Q2
                if (x->P_sets.find(T) == x->P_sets.end())
                    continue;
                if (x->P_sets.find(Q2) == x->P_sets.end())
                    return false;
            }
        }
    }
    return true;
}
bool condition_P3()
{
    bool tag = false, tag1 = false;
    State* x, * y;
    set<int> S;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q : D_set)
        {
            for (int j = 0; j < state_set.size(); j++)
            {
                y = state_set[j];
                if (y->P_sets.find(Q) != y->P_sets.end())
                    S.insert(y->ID);
            }
            if (x->P_sets.find(S) != x->P_sets.end())
            {
                if (x->P_sets.find(Q) != x->P_sets.end())
                    return false;
            }
            S.clear();
        }
    }
    return true;
}
bool condition_P4()
{
    State* x, * y;
    bool tag = false;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q1 : x->P_sets)
        {
            for (set<int> Q2 : x->P_sets)
            {
                tag = false; //tag表示是否找到y
                for (int y_id : Q2)
                {
                    y = id_state_map[y_id];
                    if (y->P_sets.find(Q1) != y->P_sets.end()) //是否存在y
                    {
                        tag = true;
                        break;
                    }
                }
                if (tag == false) //该Q2不存在y满足后鉴
                    return false;
            }
        }
    }
    return true;
}
bool condition_BP1()
{
    State* x;
    set<int> B, T1, T2, T, NQ1, NQ2, Sub;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q1 : x->P_sets)
        {
            B = x->B_set;
            for (set<int> Q2 : D_set) //在幂集中遍历Q2
            {
                set_intersection(Q1.begin(), Q1.end(), Q2.begin(), Q2.end(),
                    std::inserter(T1, T1.begin())); //Q1 交 Q2
                set_difference(state_id_set.begin(), state_id_set.end(),
                    Q1.begin(), Q1.end(), std::inserter(NQ1, NQ1.begin())); //Q1补
                set_difference(state_id_set.begin(), state_id_set.end(),
                    Q2.begin(), Q2.end(), std::inserter(NQ2, NQ2.begin())); //Q2补
                set_intersection(NQ1.begin(), NQ1.end(), NQ2.begin(), NQ2.end(),
                    std::inserter(T2, T2.begin())); //Q1补 交 Q2补
                set_union(T1.begin(), T1.end(), T2.begin(), T2.end(),
                    std::inserter(T, T.begin()));
                set_difference(B.begin(), B.end(), T.begin(), T.end(),
                    std::inserter(Sub, Sub.begin()));
                if (Sub.size() != 0) //并非子集
                    continue;
                if (x->P_sets.find(Q2) == x->P_sets.end()) //不满足后鉴
                    return false;
            }
        }
    }
    return true;
}
bool condition_BP2()
{
    State* x, * y;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q : x->P_sets)
        {
            for (int y_id : x->B_set)
            {
                y = id_state_map[y_id];
                if (y->P_sets.find(Q) == y->P_sets.end())
                    return false;
            }
        }
    }
    return true;
}
bool condition_BP3()
{
    State* x, * y;
    bool tag = false;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (int y_id : x->B_set)
        {
            y = id_state_map[y_id];
            for (set<int> Q : y->P_sets)
            {
                if (x->P_sets.find(Q) == x->P_sets.end())
                    return false;
            }
        }
    }
    return true;
}
bool condition_BP4()
{
    State* x, * y;
    bool tag = true;

    for (int i = 0; i < state_set.size(); i++) //遍历x
    {
        x = state_set[i];
        for (set<int> Q : D_set) //遍历Q
        {
            tag = true; //tag标记前鉴是否为真
            for (int j = 0; j < state_set.size(); j++) //遍历y
            {
                y = state_set[j];
                if (x->B_set.find(y->ID) != x->B_set.end())
                {
                    if (y->P_sets.find(Q) == y->P_sets.end())
                    {
                        tag = false;
                        break;
                    }
                }
            }
            if (tag == false) //前鉴为假
                continue;
            else
            {
                if (x->P_sets.find(Q) == x->P_sets.end()) //验证后鉴
                    return false;
            }
        }
    }
    return true;
}
bool condition_BP5()
{
    State* x, * y;
    bool tag = false;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q : x->P_sets)
        {
            tag = false; //tag标记是否找到y
            for (int y_id : x->B_set)
            {
                y = id_state_map[y_id];
                if (y->P_sets.find(Q) != y->P_sets.end())
                {
                    tag = true;
                    break;
                }
            }
            if (tag == false)
                return false;
        }
    }
    return true;
}
bool condition_BI1()
{
    State* x;
    set<int> B, T1, T2, T, NQ1, NQ2, Sub;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q1 : x->I_sets)
        {
            B = x->B_set;
            for (set<int> Q2 : D_set) //在幂集中遍历Q2
            {
                set_intersection(Q1.begin(), Q1.end(), Q2.begin(), Q2.end(),
                    std::inserter(T1, T1.begin())); //Q1 交 Q2
                set_difference(state_id_set.begin(), state_id_set.end(),
                    Q1.begin(), Q1.end(), std::inserter(NQ1, NQ1.begin())); //Q1补
                set_difference(state_id_set.begin(), state_id_set.end(),
                    Q2.begin(), Q2.end(), std::inserter(NQ2, NQ2.begin())); //Q2补
                set_intersection(NQ1.begin(), NQ1.end(), NQ2.begin(), NQ2.end(),
                    std::inserter(T2, T2.begin())); //Q1补 交 Q2补
                set_union(T1.begin(), T1.end(), T2.begin(), T2.end(),
                    std::inserter(T, T.begin()));
                set_difference(B.begin(), B.end(), T.begin(), T.end(),
                    std::inserter(Sub, Sub.begin()));
                if (Sub.size() != 0) //并非子集
                    continue;
                if (x->I_sets.find(Q2) == x->I_sets.end()) //不满足后鉴
                    return false;
            }
        }
    }
    return true;
}
bool condition_BI2()
{
    State* x, * y;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q : x->I_sets)
        {
            for (int y_id : x->B_set)
            {
                y = id_state_map[y_id];
                if (y->I_sets.find(Q) == y->I_sets.end())
                    return false;
            }
        }
    }
    return true;
}
bool condition_BI3()
{
    State* x, * y;
    bool tag = false;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (int y_id : x->B_set)
        {
            y = id_state_map[y_id];
            for (set<int> Q : y->I_sets)
            {
                if (x->I_sets.find(Q) == x->I_sets.end())
                    return false;
            }
        }
    }
    return true;
    return true;
}
bool condition_BI4() // (A -> B) -> C
{
    State* x, * y;
    bool tag = true;

    for (int i = 0; i < state_set.size(); i++) //遍历x
    {
        x = state_set[i];
        for (set<int> Q : D_set) //遍历Q
        {
            tag = true; //tag标记前鉴是否为真
            for (int j = 0; j < state_set.size(); j++) //遍历y
            {
                y = state_set[j];
                if (x->B_set.find(y->ID) != x->B_set.end())
                {
                    if (y->I_sets.find(Q) == y->I_sets.end())
                    {
                        tag = false;
                        break;
                    }
                }
            }
            if (tag == false) //前鉴为假
                continue;
            else
            {
                if (x->I_sets.find(Q) == x->I_sets.end()) //验证后鉴
                    return false;
            }
        }
    }
    return true;
}
bool condition_BI5()
{
    State* x, * y;
    bool tag = false;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q : x->I_sets)
        {
            tag = false; //tag标记是否找到y
            for (int y_id : x->B_set)
            {
                y = id_state_map[y_id];
                if (y->I_sets.find(Q) != y->I_sets.end())
                {
                    tag = true;
                    break;
                }
            }
            if (tag == false)
                return false;
        }
    }
    return true;
}
bool condition_BPIEF1a()
{
    State* x;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q : x->I_sets)
        {
            if (x->P_sets.find(Q) == x->P_sets.end())
                return false;
        }
    }
    return true;
}
bool condition_BPIEF1b()
{
    State* x;
    set<int> UB, B, T;

    for (int i = 0; i < state_set.size(); i++)
    {
        x = state_set[i];
        for (set<int> Q : x->I_sets) //求广义并
        {
            for (int q : Q)
                UB.insert(q);
        }
        B = x->B_set; //求RB(x)
        set_intersection(UB.begin(), UB.end(), B.begin(), B.end(),
            std::inserter(T, T.begin())); //广义并 交 RB(x)
        UB.clear();
        B.clear();
        T.clear();
        if (T.size())
            return false;
    }
    return true;
}
void ref_trans_closure() //计算自反传递闭包
{
    set<int> ref;
    pair<int, int> temp;
    set<pair<int, int> > newpairs;

    for (pair<int, int> p : RX) //ref为RX中元素的集合
    {
        ref.insert(p.first);
        ref.insert(p.second);
    }
    rt_closure = RX;

    for (int i : ref) //ref
        rt_closure.insert(make_pair(i, i));
    while (1) //trans
    {
        for (pair<int, int> x : RX)
        {
            if (x.first == x.second)
                continue;
            for (pair<int, int> y : RX)
            {
                if (y.first == y.second)
                    continue;
                if (x.second == y.first) //(x,y)，(y,z)可传递
                {
                    temp.first = x.first;
                    temp.second = y.second;
                    if (rt_closure.find(temp) == rt_closure.end())
                        newpairs.insert(temp);
                }
            }
        }
        if (newpairs.size() == 0) //集合不再变大
            break;
        else //添加新有序对
        {
            rt_closure.insert(newpairs.begin(), newpairs.end());
            newpairs.clear();
        }
    }
}
bool condition_BPIEF1c()
{
    State* x, *y, * s;
    set<int> T = state_id_set, U, C;
    bool tag;
    ref_trans_closure();
    for (int i = 0; i < state_set.size(); i++) //遍历x
    {
        x = state_set[i];
        for (int y_id : x->B_set)
        {
            for (set<int> Q : x->I_sets)
            {
                tag = false;
                for (pair<int, int> p : rt_closure)
                {
                    if (p.first == y_id && Q.find(p.second) != Q.end())
                    {
                        tag = true;
                        break;
                    }
                }
                if (tag == false)
                    return false;
            }
        }
    }
    return true;
}
bool condition_BX1()
{
    State* x, * p, * q;
    set<int> S1, S2, D;

    for (int i = 0; i < state_set.size(); i++) //遍历x
    {
        x = state_set[i];
        //求S1 = {y | (x, y) ∈ RaB ◦ RaX ◦ RaB}
        for (int p_id : x->B_set)
        {
            p = id_state_map[p_id];
            for (int q_id : p->X_set)
            {
                q = id_state_map[q_id];
                for (int y_id : q->B_set)
                {
                    S1.insert(y_id);
                }
            }
        }
        //求S2 = {y | (x, y) ∈ RaB ◦ RaX}
        for (int p_id : x->X_set)
        {
            p = id_state_map[p_id];
            for (int y_id : p->B_set)
            {
                S2.insert(y_id);
            }
        }
        //判断S1⊆S2
        set_difference(S1.begin(), S1.end(), S2.begin(), S2.end(),
            std::inserter(D, D.begin()));
        if (D.size() > 0)
            return false;
    }
    return true;
}
bool condition_BX2()
{
    State* x, * y, * u, * v;
    bool tag, front, tag1;

    for (int i = 0; i < state_set.size(); i++) //遍历x
    {
        x = state_set[i];
        for (set<int> Q : D_set) //遍历D
        {
            front = true;
            for (int y_id : x->B_set)
            {
                y = id_state_map[y_id];
                tag = false; //tag标记是否找到z
                for (int z_id : y->X_set)
                {
                    if (Q.find(z_id) != Q.end())
                    {
                        tag = true;
                        break;
                    }
                }
                if (tag == false) //找到y，不存在z满足
                {
                    front = false;
                    break;
                }
            }
            if (front == false)
                continue;
            //∀y.∃z.(x, y) ∈ RaB → ((y, z) ∈ RaX ∧ z ∈ Q)为真，检查后鉴
            for (int u_id : x->B_set)
            {
                u = id_state_map[u_id];
                tag = false; //tag标记是否找到v
                for (int v_id : u->X_set)
                {
                    v = id_state_map[v_id];
                    tag1 = false;
                    for (int w_id : v->B_set)
                    {
                        if (Q.find(w_id) == Q.end())
                        {
                            tag1 = true;
                            break;
                        }
                    }
                    if (tag1 == false)
                    {
                        tag = true;
                        break;
                    }
                }
                if (tag == false)
                    return false;
            }
        }
    }
    return true;
}
bool isSatisfied()
{
    bool tag, result = true;

    tag = condition_B3();
    result = tag && result;
    if (!tag)
        cout << "Condition B3 Conflict!" << endl;

    tag = condition_B4();
    result = tag && result;
    if (!tag)
        cout << "Condition B4 Conflict!" << endl;

    tag = condition_B5();
    result = tag && result;
    if (!tag)
        cout << "Condition B5 Conflict!" << endl;

    tag = condition_P1();
    result = tag && result;
    if (!tag)
        cout << "Condition P1 Conflict!" << endl;

    tag = condition_P2();
    result = tag && result;
    if (!tag)
        cout << "Condition P2 Conflict!" << endl;

    tag = condition_P3();
    result = tag && result;
    if (!tag)
        cout << "Condition P3 Conflict!" << endl;

    tag = condition_P4();
    result = tag && result;
    if (!tag)
        cout << "Condition P4 Conflict!" << endl;

    tag = condition_BP1();
    result = tag && result;
    if (!tag)
        cout << "Condition BP1 Conflict!" << endl;

    tag = condition_BP2();
    result = tag && result;
    if (!tag)
        cout << "Condition BP2 Conflict!" << endl;

    tag = condition_BP3();
    result = tag && result;
    if (!tag)
        cout << "Condition BP3 Conflict!" << endl;

    tag = condition_BP4();
    result = tag && result;
    if (!tag)
        cout << "Condition BP4 Conflict!" << endl;

    tag = condition_BP5();
    result = tag && result;
    if (!tag)
        cout << "Condition BP5 Conflict!" << endl;

    tag = condition_BI1();
    result = tag && result;
    if (!tag)
        cout << "Condition BI1 Conflict!" << endl;

    tag = condition_BI2();
    result = tag && result;
    if (!tag)
        cout << "Condition BI2 Conflict!" << endl;

    tag = condition_BI3();
    result = tag && result;
    if (!tag)
        cout << "Condition BI3 Conflict!" << endl;

    tag = condition_BI4();
    result = tag && result;
    if (!tag)
        cout << "Condition BI4 Conflict!" << endl;

    tag = condition_BI5();
    result = tag && result;
    if (!tag)
        cout << "Condition BI5 Conflict!" << endl;

    tag = condition_BPIEF1a();
    result = tag && result;
    if (!tag)
        cout << "Condition BPIEF1a Conflict!" << endl;

    tag = condition_BPIEF1b();
    result = tag && result;
    if (!tag)
        cout << "Condition BPIEF1b Conflict!" << endl;

    tag = condition_BPIEF1c();
    result = tag && result;
    if (!tag)
        cout << "Condition BPIEF1c Conflict!" << endl;

    tag = condition_BX1();
    result = tag && result;
    if (!tag)
        cout << "Condition BX1 Conflict!" << endl;

    tag = condition_BX2();
    result = tag && result;
    if (!tag)
        cout << "Condition BX2 Conflict!" << endl;

    return result;
}
void random_create_model()
{
    int n = state_set.size(), m = pow(2, n), t, p;
    set<int> temp;
    State* s;

    srand(time(0));
    for (int i = 0; i < n; i++)
    {
        s = state_set[i];
        for (int j = 0; j < n; j++)
        {
            t = rand() % 2;
            if (t == 1)
                s->B_set.insert(j + 1);
        }
        p = rand() % m;
        while (s->P_sets.size() < p)
        {
            for (int k = 0; k < n; k++)
            {
                t = rand() % 2;
                if (t == 1)
                    temp.insert(k + 1);
            }
            if (temp.size() == 0)
                continue;
            s->P_sets.insert(temp);
            temp.clear();
        }
        p = rand() % m;
        while (s->I_sets.size() < p)
        {
            for (int k = 0; k < n; k++)
            {
                t = rand() % 2;
                if (t == 1)
                    temp.insert(k + 1);
            }
            if (temp.size() == 0)
                continue;
            s->I_sets.insert(temp);
            temp.clear();
        }
        for (int j = 0; j < n; j++)
        {
            t = rand() % 2;
            if (t == 1)
                s->X_set.insert(j + 1);
        }
    }
}
void outfile()
{
    fstream out2;
    State* s;

    out2.open("file2.txt", ios::out);
    if (out2.fail())
    {
        cout << "cannot open the file!" << endl;
        exit(0);
    }
    //输出模型状态集
    for (int i = 0; i < state_set.size(); i++)
    {
        s = state_set[i];
        out2 << 's' << s->ID << endl;

        for (set<char>::iterator p = s->atom_set.begin(); p != s->atom_set.end(); p++)
            out2 << 's' << *p << ' ';

        for (set<int>::iterator p = s->B_set.begin(); p != s->B_set.end(); p++)
            out2 << 's' << *p << ' ';
        out2 << '#' << endl;

        for (set<set<int> >::iterator p = s->P_sets.begin(); p != s->P_sets.end(); p++)
        {
            for (set<int>::iterator q = p->begin(); q != p->end(); q++)
                out2 << 's' << *q << ' ';
            out2 << "# ";
        }
        if (s->P_sets.size() == 0)
            out2 << '#';
        out2 << endl;

        for (set<set<int> >::iterator p = s->I_sets.begin(); p != s->I_sets.end(); p++)
        {
            for (set<int>::iterator q = p->begin(); q != p->end(); q++)
                out2 << 's' << *q << ' ';
            out2 << "# ";
        }
        if (s->I_sets.size() == 0)
            out2 << '#';
        out2 << endl;

        for (set<int>::iterator p = s->X_set.begin(); p != s->X_set.end(); p++)
            out2 << 's' << *p << ' ';
        out2 << '#' << endl;
        out2 << endl;
    }
    out2.close();
}
void find_model()
{
    int no, n = 3;
    State* state;
    char ch;

    while (1)
    {
        no = 1;
        for (int i = 0; i < n; i++)
        {
            state_id_set.insert(no);
            state = new State;
            state->ID = no++;
            state_set.push_back(state);
            id_state_map[state->ID] = state;
        }
        random_create_model();
        ModelPrint();
        if (isSatisfied())
        {
            cout << "Find a proper model!" << endl;
            cout << "是否输出至文件[Y/N]" << endl;
            cin >> ch;
            if (toupper(ch) == 'Y')
                outfile();
            break;
        }
        else
        {
            //system("pause");
            cout << endl << endl;
        }
        state_set.clear();
        state_id_map.clear();
        id_state_map.clear();
        state_id_set.clear();
        D_set.clear();
        RX.clear();
        rt_closure.clear();
    }
}
#endif ModelCreate
